大西琢朗; "論理学上級Ⅱ, 様相論理のシークエント計算"
https://sites.google.com/site/onishitakuro/teaching/2018nian-du-lun-li-xue-shang-jiii
大西琢朗
メモ
Sara Negri
による?
古典命題論理
の
シークエント計算
$ \bf {G3c}
における
カット除去定理
命題論理
の
カット除去
に関しては一番わかりやすい解説だった気がする
Gentzenのシークエント計算
$ \bf LK
に公理規則として素朴に
$ \sf K
公理を付け足すと,まあ論理
$ \bf K
と完全性は成り立つが,
カット除去
は成り立たない.
始式として公理を付け加えた様相論理のシークエント計算体系
いくつかの
様相論理の公理
に対して完全になる規則を考えることは出来るが,例えば
$ \sf D \equiv \Box A \to \Diamond A
のようなものでは
部分論理式特性
が成り立たない.
様相論理S5
に至っては規則があっても
カット除去
ができなくなる.
規則を付け加えた様相論理のシークエント計算体系
Sara Negri
による
ラベル付きシークエント計算
というものを考えて
様相論理のシークエント計算
を考える.
メモ: 参考文献
K. Bednarska, A. Indrzejczak; "Hypersequent Calculi for S5: The Methods of Cut Elimination"
$ \bf S5
のハイパーシークエント計算のバラエティについて